es:ES, P:(E), j:E. (e:E. e c j  Dec(P(e)))  Dec(k:E. k c j  P(k)) 

latex

Definitions	x. t(x), A c B, P  Q, P & Q, P  Q, t  T, x(s), P  Q, , x:A. B(x), P  Q, e c e'
Lemmas	decidable alle-causl, decidable and, decidable functionality, es-causle weakening, es-le weakening eq, es-causle weakening locl, es-causl wf, event system wf, decidable wf, es-causle wf, es-E wf